00100 00200 R(D(X1 O) X1); 00300 R(D(X1 X1) O); 00400 R(D(O X1) O); 00500 R(D(X1 U) O); 00550 R(D(U D(U X1))D(X1 D(U X1))); 00600 ;